//
//$Id: fa_equiv.cpp 630 2011-01-27 17:40:06Z andrew.tsyganov $
#include "stdafx.h"
#include "contrib/simpleini/simpleini.h"
#include "../fa.h"
#include "../utils.h"
#include "../my_time.h"

using namespace std;

bool SaveToGAP(vector<FA> const& v_fa, Subset const& s)
{
    ofstream ofs;
    ofs.open ("automata.g", ofstream::out);

    if (ofs.fail())
    {
        cout << "SaveToGAP: file open error!" << endl;
        return false;
    }

    cout << "Writing GAP program to 'automata.g'... ";

    ofs << "LogTo(\"gap_log.txt\");" << endl
        << endl;

    size_t n = v_fa.size();

    for (size_t i = 0; i < n; ++i)
    {
        if (!s.empty() && !s.contains(i))
            continue;
        
        ofs << setw(20) << left << v_fa[i].name_ << " := " << v_fa[i].to_GAP() << endl;
    }

    ofs << endl
        << "automata := [";

    string str;

    for (size_t i = 0; i < n; ++i)
    {
        if (!s.empty() && !s.contains(i))
            continue;
        
        str = str + v_fa[i].name_ + ", "; 
    }

    str.erase(str.length()-2, 2);

    ofs << str << "];" << endl
        << endl
        << "names := [";

    str = "";

    for (size_t i = 0; i < n; ++i)
    {
        if (!s.empty() && !s.contains(i))
            continue;
        
        str = str + "\"" + v_fa[i].name_ + "\", "; 
    }

    str.erase(str.length()-2, 2);

    ofs << str << "];" << endl
        << endl
        << "EqClasses := function(automata, names)" << endl
        << "    local eca, ecn, n, m, i, j, t, a, equiv_found;" << endl
        << "    eca := [[automata[1]]];" << endl
        << "    ecn := [[names[1]]];" << endl
        << "    n := Length(automata);" << endl
        << "    for i in [2..n] do" << endl
        << "        m := Length(eca);" << endl
        << "        equiv_found := false;" << endl
        << "        for j in [1..m] do" << endl
        << "            t := eca[j];" << endl
        << "            a := t[1];" << endl
        << "            if AreEquivAut(a, automata[i]) then" << endl
        << "                equiv_found := true;" << endl
        << "                Add(eca[j], automata[i]);" << endl
        << "                Add(ecn[j], names[i]);" << endl
        << "                break;" << endl
        << "            fi;" << endl
        << "        od;" << endl
        << "        if equiv_found = false then" << endl
        << "            Add(eca, [automata[i]]);" << endl
        << "            Add(ecn, [names[i]]);" << endl
        << "        fi;" << endl
        << "    od;" << endl
        << "    return [eca, ecn];" << endl
        << "end;" << endl
        << endl
        << "res := EqClasses(automata, names);" << endl
        << "res_names := res[2];" << endl
        << "n := Length(res_names);" << endl
        << "Print(\"Equivalenve classes (\", n, \"):\\n\");" << endl
        << "for i in [1..n] do" << endl
        << "    Display(res_names[i]);" << endl
        << "od;" << endl;

    ofs.close();    

    cout << "done." << endl;

    return true;
}


void CheckEquivalence(vector<FA> const& v_fa, Subset const& s)
{
    if (!s.empty())
        cout << "Consider automata: " << s.to_String(NO_BRACKETS) << "." << endl;
    else
        cout << "Consider all automata in the folder." << endl;

    cout << "Determinizing automata... ";

    double start_time = get_time();

    vector<FA> v_dfa;
    vector<Subset> v_s;

    size_t n = v_fa.size();
    v_dfa.resize(n);

    for (size_t i = 0; i < n; ++i)
    {
        if (!s.empty() && !s.contains(i))
            continue;

        MinimizeBrzozowski(v_fa[i], v_dfa[i], "m");
        //Determinize(v_fa[i], v_dfa[i], v_s, "d");
    }

    double end_time = get_time();

    cout << "done." << endl
         << "Determinization time = " << end_time - start_time << " s." << endl
         << "Checking equivalence... " << flush;

    v_s.clear();

    size_t f = (s.empty() ? 0 : s.get_first());
    
    v_s.reserve(n);
    v_s.resize(1);
    v_s[0].insert(f);

    size_t count = 0;
    start_time = get_time();
    for (size_t i = f+1; i < n; ++i)
    {
        if (!s.empty() && !s.contains(i))
            continue;

        //cout << v_fa[i].name_ << endl;

        bool equiv_found = false;

        for (size_t j = 0; j < v_s.size(); ++j)
        {
            size_t k = v_s[j].get_first();

            //double start_time2 = get_time();
            //bool equiv = EquivalentDFAs(v_dfa[k], v_dfa[i]);
            vector<Subset> v;
            bool equiv = IsomorphicDFAs(v_dfa[k], v_dfa[i], v);
            ++count;
            //double end_time2 = get_time();

            //cout << left << setw(25) << v_dfa[i].name_ << " and " << setw(25) << v_dfa[k].name_ << setw(10) << " equiv: " << equiv << " check time = " 
            //     << end_time2 - start_time2 << endl; 

            if (equiv)
            {
                v_s[j].insert(i);
                equiv_found = true;
                break;
            }
        }

        if (!equiv_found)
        {
            Subset c;
            c.insert(i);
            v_s.push_back(c);
        }
    }
    end_time = get_time();

    cout << "done, " << count << " checks made." << endl
         << "Check time = " << fixed << end_time - start_time << " s." << endl
         << endl;

    size_t m = v_s.size();

    cout << "Equivalence classes (" << m << "):" << endl
         << endl;

    for (size_t i = 0; i < m; ++i)
    {
        size_t k = v_s[i].count();
        cout << "  Class " << i << " (" << k << "):" << endl;

        for (size_t j = 0; j < k; ++j)
            cout << "    " << v_fa[v_s[i].get_By_Count(j)].name_ << endl;

        cout << endl;
    }
}

int main(int argc, char* argv[])
{

    if (argc < 2)
    {
        cout << "fa_equiv usage: fa_equiv.exe dir_name [n1 [n2 [n3 [...]]]]" << endl;
        return -1;
    }

    vector<FA> v_fa;

    cout << "Reading automata from '" << argv[1] << "' folder... ";
    LoadFAs(v_fa, argv[1]);
    cout << "done, " << v_fa.size() << " automata read." << endl;

    if (!v_fa.empty())
    {
        Subset s;

        for (int i = 2; i < argc; ++i)
            s.insert((size_t) atoi(argv[i]));

        //s.set(0);
        //s.set(10);

        SaveToGAP(v_fa, s);
        CheckEquivalence(v_fa, s);
    }
 
    return 0;
}
//EOF!